\label{formalGrounds}

In this section, we build a formal definition of DSLTrans in
order to provide a clear specification of our language and a basis for studying and proving
properties about it. In the mathematical theory we disregard the formalization
of: class attributes (a particular case of named relations); and negative
conditions (a particular case of positive ones). We present a light
formalization of the relations at the metamodel and model levels which deals
only with the difference between reference and containment relations between
classes. These non formalized --- but implemented in~\cite{dsltransplugin} ---
features of the language do not affect the termination or confluence properties
of our language.

\begin{definition}{Typed Graph and Indirect Typed Graph}
\label{def:typed_graph}

A typed graph is a 4-tuple $\langle V,E,\tau_{V},\tau_{E} \rangle$ where $V$ is
a finite set of vertices, $E\subseteq V\times V$ is a finite set of directed
edges connecting the vertices, $\tau_{V}: V \rightarrow Type_{V}$ is a
surjective typing function for the elements of V, and $\tau_{E}: E \rightarrow
Type_{E}$  is a surjective typing function for the elements of E. Edges
$(v,v')\in E$ are noted $v\rightarrow v'$. The set of all typed graphs is called
$TG$.

An indirect typed graph is a 5-tuple $\langle V,E,\tau_{V},\tau_{E},Il\rangle$,
where $\langle V,E,\tau_{V},\tau_{E}\rangle$ is a typed graph and $Il\subseteq
E$ is a set of edges called \emph{indirect links}. The set of all indirect typed
graphs is called $ITG$.
\end{definition}

\begin{definition}{Typed Graph Union}
\label{def:typed_graph_union}

Let $\langle V,E,\tau_{V},\tau_{E}\rangle,\langle
V',E',\tau'_{V},,\tau'_{E}\rangle\in TG$ be typed graphs. The typed graph union
is the function $\sqcup :TG\times TG\rightarrow TG$ defined as: $\langle
V,E,\tau_{V},\tau_{E}\rangle\;\sqcup\;\langle
V',E',\tau'_{V},\tau'_{E}\rangle=\langle V\cup V', E\cup E', \tau_{V} \cup
\tau'_{V},\tau_{E} \cup \tau'_{E}\rangle$
\end{definition}

\begin{definition}{Transitive Closure, Undirected Transitive Closure}
\label{def:transitive_closure}

The transitive closure set over a set of edges $E$, noted $E^{*}$,
is the largest set recursively defined by the following conditions:\\
a) if $s \rightarrow s' \in E$ then $s \rightarrow s' \in E^{*}$,\\
b) if $\{s \rightarrow s', s' \rightarrow s''\} \subseteq E^{*}$ then $s
\rightarrow s'' \in E^{*}$.

Given $E^{*}$, the undirected transitive closure of $E$, noted
$E^{*}_{\leftrightarrow}$, is the least set such that if $s \rightarrow s'
\in E^{*}$ then $\{s \rightarrow s', s' \rightarrow s\}\subseteq
E^{*}_{\leftrightarrow}$.
\end{definition}

\begin{definition}{Typed Subgraph}
\label{def:typedsubgraph}

Let $\langle V,E,\tau_{V},\tau_{E}\rangle=g,\langle
V',E',\tau'_{V},\tau'_{E}\rangle=g'\in TG$ be typed graphs. A typed graph $g'$
is a typed subgraph of $g$, written $g'\blacktriangleleft g$, iff $V'\subseteq V$,
$E'\subseteq E$, $\tau'_{V}=\tau_{{V}_{|V'}}$, and
$\tau'_{E}=\tau_{{E}_{|E'}}$, where the $|$ operator restricts the domain of
a typing function to a subset of vertices (resp. edges) of the typing function's
original domain.
\end{definition}

\begin{definition}{Connected Typed Subgraph}
\label{def:connected_typed_graph}

Let $\langle V,E,\tau_{V},\tau_{E}\rangle=g,\langle
V',E',\tau'_{V},\tau'_{E}\rangle=g'\in TG$ be typed graphs. $g$ is a connected
typed subgraph of $g'$ w.r.t a set of relations $L \subseteq E'$, written $g
\blacktriangleleft_{\leftrightarrow\;L} g'$, iff the following conditions are
satisfied:\\
a) $V \subseteq V'$,\\
b) $E \subseteq L$,\\
c) $\tau_{V} \subseteq \tau'_{V}$,\\
d) $\tau_{E} \subseteq \tau'_{E}$,\\
e) $\forall v, v' \in V: v \rightarrow v' \in L^{*}_{\leftrightarrow}$.
\end{definition}

% \marginpar{esta definicao 5 pode ser feita sem recorrer a estender
% o typed graph, o que nao e muito elegante. Na verdade o que se quer e mais a
% frente utilisar os backward links como restricao a construcao de grafos
% conexos.}

For instance, if we have two typed graphs $g$ and $g'$ (where $g = \langle
V,E,\tau_{V},\tau_{E} \rangle \in TG$ and $g' = \langle
V',E',\tau'_{V},\tau'_{E} \rangle \in TG$), and also a set of edges such that
$Link \subseteq E'$, then $g \blacktriangleleft_{\leftrightarrow\;Link} g'$
means that $g$ is a connected typed subgraph of $g'$, where $E$ will only be
formed of connected edges of $Link$, and consequently shape the possible
vertices of $V$ and $\tau$ according to $E$ edges.

\marginpar{i(bfb) am not sure about this definition
\ref{def:typed_graph_equivalence}, since we are only taking into account both
the typing functions, and not really the existence of the vertices and edges on
the co-domain of the isomorphism.}

\begin{definition}{Typed Graph Equivalence}
\label{def:typed_graph_equivalence}

Let $\langle V,E,\tau_{V},\tau_{E}\rangle=g,\langle
V',E',\tau'_{V},\tau'_{E}\rangle=g'\in TG$ be typed graphs. $g$ and $g'$ are
equivalent, written $g\cong g'$, iff there is a graph isomorphism
$f:V\rightarrow V'$ of graphs $\langle V,E\rangle$ and $\langle V',E'\rangle$
such that the following conditions are satisfied:\\
a) $\forall v\in V\;.\;\tau_{V}(v)=\tau'_{V}(f(v))$\\
b) $\forall e=(v_{s} \rightarrow v_{t})\in E\;.\;\tau_{E}(e)=\tau'_{E}((f(v_{s})
\rightarrow f(v_{t})))$\\ 
c) $\forall v'\in V'\;.\;\tau'_{V}(v')=\tau_{V}(f^{-1}(v'))$\\ 
d) $\forall e'=(v_{s} \rightarrow v_{t})\in
E'\;.\;\tau'_{E}(e')=\tau_{E}((f^{-1}(v_{s})\rightarrow f^{-1}(v_{t})))$\\
\end{definition}

More informally, two typed graphs are defined equivalent if they have the same
shape and related vertices and edges have the same type.

\marginpar{Typed Graph Strict Instance definition was removed since it was not
being used--- and probably won't be used in this paper.. still its commented}

% \begin{definition}{Typed Graph Strict Instance}
% \label{def:typed_graph_strict_instance}
% 
% Let $\langle V,E,\tau\rangle=g,\langle V',E',\tau\rangle=g'\in TG$ be typed
% graphs. $g'$ is a typed graph strict instance of $g$, written $g'\Vvdash g$, iff
% there is a surjective graph homomorphism $f:V'\rightarrow V$ (meaning that if
% $v'_{1}\rightarrow v'_{2}\in E'$ then $f(v'_{1})\rightarrow f(v'_{2})\in E$)
% such that if $v'\in V'$ then $\tau(v')=\tau(f(v'))$.
% 
% \end{definition}

\marginpar{Definition \ref{def:typed_graph_left_merge} must be revised to tackle
its real use in the backward-link cut operator definition.}

\begin{definition}{Typed Graph Merge}
\label{def:typed_graph_left_merge}

Let $l$, $m$, $r$ be typed graphs, respectively named the \emph{left},
\emph{merge} and \emph{right} graphs. The typed graph left merge is the relation
$\sqcup_{TG} \subseteq TG \times TG \times TG \rightarrow TG$ defined as
follows: $$l \sqcup_{m} r = l \sqcup r_{\Delta}$$ 
\begin{center}
where $(m' \sqcup r_{\Delta}) \cong r$ given that $m' \blacktriangleleft l$ and
$m' \cong m$. Note that $\{r_{\Delta},m'\} \subseteq TG$.
\end{center}
\end{definition}

Informally, we can merge two graphs $l$ and $r$ using only the parts that
are common to both. The common parts are determined by graph $m$.

\begin{definition}{Naming Function}
\label{def:naming_function}


\end{definition}


\begin{definition}{Metamodel, Inherits and $\leq$}
\label{def:metamodel}

A \textbf{metamodel} $pm = \langle V,E,\tau_{V},\tau_{E}\rangle\in TG$ is a
typed graph where $\tau_{V}$ is a bijective typing function $\tau_{V}: V
\rightarrow ClassName \times \{ abstract, concrete \}$, and $\tau_{E}$ is a
surjective typing function $\tau_{E}: E \rightarrow AssociationName \times \{
inherits, reference, containment \}$ such that for all $e=(v_{s} \rightarrow
v_{t}) \in E$, if there exists $e'=(v_{s} \rightarrow v'_{t}) \in E$ where
$\tau_{E}(e) = \tau_{E}(e')$, then $v_{t} = v'_{t}$. Also, the subgraph $\langle
V,\{ e=(v\rightarrow v')\;\in\;E|\tau_{E}(e)=(\_,inherits) \}\rangle$ is
acyclic.

The relation $Inherits_{mm}: (ClassName \times \{ abstract, concrete
\}) \times (ClassName \times \{ abstract, concrete \})$ is defined w.r.t. $mm$
such that if $e = (v_{s} \rightarrow v_{t}) \in E^{*}$ and
$\tau_{E}(e)=(\_,inherits)$, then $(\tau_{V}(v_{s}),\tau_{V}(v_{t}))\;\in\;
Inherits_{mm}$.

The partial order relation $\leq_{mm}$ uses the above defined relation
such that: $\leq_{mm} = Inherits_{mm}^{*} \cup \{ (\tau_{V}(v),\tau_{V}(v)) | v
\in V \}$, having that if $(a,b),(b,a) \in \leq_{mm}$ then $a = b$ (i.e it must
not have inheritance cycles). In order to be a partial order relation,
$\leq_{pm}$ must be reflexive, transitive and antisymmetric (notice that in
order to be antisymmetric we needed to impose that in metamodels the
subgraph formed by $\langle V,\{ e=(v\rightarrow
v')\;\in\;E|\tau_{E}(e)=(\_,inherits) \}\rangle$ is acyclic).

The set of all metamodels is called META.

\end{definition}


\begin{definition}{Pattern and Model}
\label{def:patternmodel}

A pattern $\langle V,E,\tau_{V},\tau_{E}\rangle$ is a typed graph where
$\tau_{V}$ is a surjective typing function $\tau_{V}: V \rightarrow ClassName
\times \{ concrete, abstract \}$, and $\tau_{E}$ is also a surjective typing
function $\tau_{E}: E \rightarrow AssociationName \times \{ reference,
containment \}$ such that the subgraph $\langle V,\{ e=(v\rightarrow
v')\;\in\;E|\tau_{E}(e)=(\_,containment) \}\rangle$ is acyclic\footnote{By using
\emph{containment} and \emph{reference} as types for edges we allow modeling the
different types of associations between the elements of patterns, metamodels or
models. In particular, the fact that the subgraph of containment relations in a
typed graph is acyclic models EMF containment associations.}.
The set of all patterns is called $PAT$.

A model, is a pattern $\langle V,E,\tau_{V},\tau_{E}\rangle$ where $\tau_{V}$ is
a surjective typing function $\tau_{V}: V \rightarrow ClassName \times \{
concrete \}$. The set of all models is called $MODEL$.
\end{definition}

\begin{definition}{Pattern/Model Instance}
\label{def:model_instance}

Let $\langle V,E,\tau_{V},\tau_{E}\rangle = mm\;\in\;META$ be a metamodel, and 
$\langle V',E',\tau'_{V},\tau'_{E} \rangle=pat\;\in\;PAT$ be a pattern (in
particular it can also be a model). $pat$ is an instance of $mm$, written $pat
\Vdash mm$, iff for all $v_{1}'\rightarrow v_{2}'\in E'$ there is a
$v_{1}\rightarrow v_{2}\in E$ such that:\\ 
a) $\tau'_{V}(v_{1}') \leq_{mm} \tau_{V}(v_1)$,\\
b) $\tau'_{V}(v_{2}') \leq_{mm} \tau_{V}(v_2)$,\\
c) $\tau'_{E}(v_{1}'\rightarrow v_{2}')=\tau_{E}(v_{1}\rightarrow v_{2})$.
 
The set of all pattern instances of a metamodel $M$ is called $PAT^{M}$.
The set of all model instances of a metamodel $M$ is called $MODEL^{M}$.
\end{definition}

Notice that we only enforce that connections between vertices of $mm$ must exist
also in $pat$ and have the same type or inherited type.

\begin{definition}{Match-Apply Model}
\label{def:match_apply_model}

A Match-Apply Model is a 7-tuple $mam = \langle V,E,\tau_{V},\tau_{E},
Match,Apply,Bl\rangle \in TG$, 
where $Match=\langle V',E',\tau_{V}',\tau_{E}'\rangle \in MODEL$ is a model,
and $Apply=\langle V'',E'',\tau_{V}'',\tau_{E}''\rangle \in MODEL$ is a model,
such that $V',V'' \subseteq V$, $E',E'' \subseteq E$, $\tau_{V}',\tau_{V}''
\subseteq \tau_{V}$, and $\tau_{E}',\tau_{E}'' \subseteq \tau_{E}$. 
Edges $Bl\subseteq V'\times V''\subseteq E$ are called \emph{backward links}. 

The above $mam$ Match-Apply Model is defined for a \emph{source} metamodel $s$
and a \emph{target} metamodel $t$ (written $mam^{s}_{t}$) iff $Match \Vdash s$
and $Apply \Vdash t$. 

The set of all Match-Apply models for a source metamodel
$s$ and a target metamodel $t$ is called $MAM^{s}_{t}$. Vertices in the $Apply$
model which are not connected to \emph{backward links} are called \emph{free
vertices}. The $back:MAM^{s}_{t}\rightarrow MAM^{s}_{t}$ function connects all
vertices in the $Match$ model to all \emph{free} vertices with \emph{backward
link} edges.

\end{definition}

The $Match$ part of a match-apply model is used to hold the immutable source
model during a transformation. The $Apply$ part is used to hold the intermediate
results of the transformation.

\begin{definition}{Transformation Rule}
\label{def:transformation_rule}

A Transformation Rule is a 8-tuple $\langle
V,E,\tau_{V},\tau_{E},Match,Apply,Bl,Il\rangle$, where $\langle
V,E,\tau_{V},\tau_{E},Match,Apply,Bl\rangle \in MAM^{s}_{t}$ is a match-apply
model, except for $Match=\langle V',E',\tau'_{V},\tau'_{E} \rangle \in PAT$
which now is a pattern, and the edges $Il\subseteq E$ are called \emph{indirect
links}. The set of all transformation rules defined for a source metamodel $s$
and a target metamodel $t$ is called $TR^{s}_{t}$. The
$strip:TR^{s}_{t}\rightarrow TR^{s}_{t}$ function removes from a transformation
rule all \emph{free} vertices and associated edges.

\end{definition}

We define a \emph{transformation rule} as a kind of match-apply model
which allows \emph{indirect links} in the $match$ pattern.

\begin{definition}{Subgraph relation between Match-Apply models and
Transformation Rules}
\label{def:subgraph_mam_tr}

A transformation rule $tr = \langle
V',E',\tau'_{V},\tau'_{E},Match',Apply',Bl',Il\rangle \in TR^{s}_{t}$ is
considered a typed indirect subgraph of a match-apply model\\ 
$mam = \langle V,E,\tau_{V},\tau_{E}, Match,Apply,Bl\rangle \in MAM$, written
$tr \lhd mam$ iff:

\begin{enumerate}
\item $\langle V',E'\setminus Il,\tau'_{V},\tau'_{E}\rangle \blacktriangleleft
\langle V, E,\tau_{V},\tau_{E}\rangle$
\item if $v'_{s}\rightarrow v'_{t}\in Il$ then there exists $v_{s}\rightarrow
v_{t}\in E_{c}^{*}$ where $\tau'_{V}(v'_{s})=\tau_{V}(v_{s})$,
$\tau'_{V}(v'_{t})=\tau_{V}(v_{t})$ and $E_{c}^{*}$ is obtained by the
transitive closure of $E_{c}=\{v_{s}\rightarrow v_{t}\in
E|\tau_{E}(v_{s}\rightarrow v_{t})=(\_,containment)\}$.
\end{enumerate}

\end{definition}

\begin{definition}{Property}

A Property is a 8-tuple $\langle V,E\cup
Il,\tau_{V},\tau_{E},Match,Apply,Bl,Il\rangle$,\\ 
where $\langle V,E,\tau_{V},\tau_{E},Match,Apply,Bl\rangle \in MAM^{s}_{t}$ is a
match-apply model. $Match=\langle V',E',\tau'_{V},\tau'_{E}\rangle \in PAT^{s}$
is a pattern, $Apply=\langle V'',E'',\tau''_{V},\tau''_{E}\rangle \in MODEL^{t}$
and the edges $Il\subseteq (V'\times V')\cup (V''\times V'')$ are called
\emph{indirect links}. The set of all properties having source metamodel $s$ and
target metamodel $t$ is called $Property^{s}_{t}$.
\end{definition}

The language to describe properties is in fact very similar to the language to
express transformations, with the additional possibility of expressing indirect
links in the $apply$ pattern --- thus allowing more abstract patterns than the
ones expressed in transformations. This is natural given that the properties of
a transformation can be more abstract than the rules implementing them.

\begin{definition}{Layer, Transformation}
\label{def:layer_transformation}

A layer is a finite set of transformation rules  $tr\subseteq TR^{s}_{t}$. The
set of all layers  for a source metamodel $s$ and a target metamodel $t$  is
called $Layer^{s}_{t}$. A transformation is a finite list of layers denoted
$[l_{1}::l_{2}::\ldots::l_{n}]$ where $l_{k}\in Layer^{s}_{t}$ and $1\leq k \leq
n$. The set of all transformations for a source metamodel $s$ and a target
metamodel $t$  is called $Transformation^{s}_{t}$.
\end{definition}

At the transformation level, the transformation rules have to be unfolded into
several ones according to the elements present in the match pattern and its
respective match metamodel. Therefore, we use the unfold operator that is
next defined for transformations, layers and rules.

\begin{definition}{Inheritance Unfold}
\label{def:layer_transformation_inheritance}

The unfold function when applied on a transformation
$[l_{1}::l_{2}::\ldots::l_{n}] \in Transformation^{s}_{t}$ returns another
transformation $[unfold(l_{1})::unfold_(l_{2})::\ldots::unfold_(l_{n})] \in
Transformation^{s}_{t}$.\\

The unfold function when applied on a layer (which we can subdivide into a set
union of rules) $\bigcup_{i=1}^{n} r_{i} \in \mathcal{P}(TR^{s}_{t})$ returns
another set $\bigcup_{i=1}^{n} \bigcup unfold(r_{i}) \in
\mathcal{P}(TR^{s}_{t})$, which is again considered a new layer.\\

The unfold function when applied on a single rule $unfold(\langle
V,E,\tau_{V},\tau_{E}\rangle) \in TR^{s}_{t}$ returns a set of rules $\{
\langle V,E,\tau_{V}',\tau_{E}\rangle \in TR^{s}_{t}\} $, where the new typing
function $\tau_{V}' \in \mathcal{P}(V \times (Type \times \{
concrete\}))$ is such that $\tau_{V}' = \{ \bigcup_{i=1}^{n}(v_{i},t_{i}')
\;|\; \tau_{V} = \bigcup_{i=1}^{n}(v_{i},t_{i}) \land \bigwedge_{i=1}^{n}(t_{i}' \leq t_{i}) \}\\
$
\end{definition}

Notice that in the above definition the $\leq$ operator implicitly uses the
source metamodel $s$ (which we discard due to excess notation). Also note
that the new typing function do not possess anymore the ability to reference
abstract classes, which means that our unfolded rules will only have concrete
classes in both match and apply parts.

We naturally extend the notion of union (definition~\ref{def:typed_graph_union})
to patterns and models (definition~\ref{def:patternmodel}), match-apply models
(definition~\ref{def:match_apply_model}) and transformation rules
(definition~\ref{def:transformation_rule}). Finally, we extend the notion
of typed graph equivalence (definition~\ref{def:typed_graph_equivalence}) to
transformation rules (definition~\ref{def:transformation_rule}).
